YES 1.526 H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/empty.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:



HASKELL
  ↳ BR

mainModule Main
  ((elem :: (Eq a, Eq b) => (b,a ->  [(b,a)]  ->  Bool) :: (Eq b, Eq a) => (b,a ->  [(b,a)]  ->  Bool)

module Main where
  import qualified Prelude



Replaced joker patterns by fresh variables and removed binding patterns.

↳ HASKELL
  ↳ BR
HASKELL
      ↳ COR

mainModule Main
  ((elem :: (Eq b, Eq a) => (a,b ->  [(a,b)]  ->  Bool) :: (Eq b, Eq a) => (a,b ->  [(a,b)]  ->  Bool)

module Main where
  import qualified Prelude



Cond Reductions:
The following Function with conditions
undefined 
 | False
 = undefined

is transformed to
undefined  = undefined1

undefined0 True = undefined

undefined1  = undefined0 False



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
HASKELL
          ↳ Narrow

mainModule Main
  (elem :: (Eq b, Eq a) => (b,a ->  [(b,a)]  ->  Bool)

module Main where
  import qualified Prelude



Haskell To QDPs


↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ Narrow
            ↳ AND
QDP
                ↳ QDPSizeChangeProof
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primPlusNat(Succ(xv3300), Succ(xv4011000)) → new_primPlusNat(xv3300, xv4011000)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ Narrow
            ↳ AND
              ↳ QDP
QDP
                ↳ QDPSizeChangeProof
              ↳ QDP
              ↳ QDP
              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primMulNat(Succ(xv31100), Succ(xv401100)) → new_primMulNat(xv31100, Succ(xv401100))

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ Narrow
            ↳ AND
              ↳ QDP
              ↳ QDP
QDP
                ↳ QDPSizeChangeProof
              ↳ QDP
              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primEqNat(Succ(xv3100), Succ(xv40100)) → new_primEqNat(xv3100, xv40100)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ Narrow
            ↳ AND
              ↳ QDP
              ↳ QDP
              ↳ QDP
QDP
                ↳ QDPSizeChangeProof
              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_esEs1(@2(xv30, Just(xv310)), @2(xv400, Just(xv4010)), he, app(ty_Maybe, app(app(ty_Either, bac), bad))) → new_esEs0(xv310, xv4010, bac, bad)
new_esEs(@3(xv310, xv311, xv312), @3(xv4010, xv4011, xv4012), ba, bb, app(app(ty_Either, bf), bg)) → new_esEs0(xv312, xv4012, bf, bg)
new_esEs1(@2(xv30, Just(xv310)), @2(xv400, Just(xv4010)), he, app(ty_Maybe, app(ty_Maybe, bag))) → new_esEs2(xv310, xv4010, bag)
new_esEs2(Just(xv310), Just(xv4010), app(app(app(ty_@3, hh), baa), bab)) → new_esEs(xv310, xv4010, hh, baa, bab)
new_esEs3(:(xv310, xv311), :(xv4010, xv4011), app(ty_[], bcb)) → new_esEs3(xv310, xv4010, bcb)
new_esEs1(@2(xv30, xv31), @2(xv400, xv401), app(ty_[], bdd), bcf) → new_esEs3(xv30, xv400, bdd)
new_esEs1(@2(xv30, xv31), @2(xv400, xv401), app(app(ty_Either, bcg), bch), bcf) → new_esEs0(xv30, xv400, bcg, bch)
new_esEs1(@2(xv30, @3(xv310, xv311, xv312)), @2(xv400, @3(xv4010, xv4011, xv4012)), he, app(app(app(ty_@3, ba), app(ty_[], df)), cg)) → new_esEs3(xv311, xv4011, df)
new_esEs0(Right(xv310), Right(xv4010), gc, app(app(ty_@2, ha), hb)) → new_esEs1(xv310, xv4010, ha, hb)
new_esEs(@3(xv310, xv311, xv312), @3(xv4010, xv4011, xv4012), ba, app(ty_Maybe, de), cg) → new_esEs2(xv311, xv4011, de)
new_esEs1(@2(xv30, @3(xv310, xv311, xv312)), @2(xv400, @3(xv4010, xv4011, xv4012)), he, app(app(app(ty_@3, app(app(ty_Either, eb), ec)), bb), cg)) → new_esEs0(xv310, xv4010, eb, ec)
new_esEs1(@2(xv30, :(xv310, xv311)), @2(xv400, :(xv4010, xv4011)), he, app(ty_[], app(app(ty_Either, bbe), bbf))) → new_esEs0(xv310, xv4010, bbe, bbf)
new_esEs2(Just(xv310), Just(xv4010), app(ty_Maybe, bag)) → new_esEs2(xv310, xv4010, bag)
new_esEs1(@2(xv30, @3(xv310, xv311, xv312)), @2(xv400, @3(xv4010, xv4011, xv4012)), he, app(app(app(ty_@3, ba), app(app(app(ty_@3, cd), ce), cf)), cg)) → new_esEs(xv311, xv4011, cd, ce, cf)
new_esEs1(@2(xv30, xv31), @2(xv400, xv401), app(ty_Maybe, bdc), bcf) → new_esEs2(xv30, xv400, bdc)
new_esEs3(:(xv310, xv311), :(xv4010, xv4011), app(app(app(ty_@3, bbb), bbc), bbd)) → new_esEs(xv310, xv4010, bbb, bbc, bbd)
new_esEs3(:(xv310, xv311), :(xv4010, xv4011), bba) → new_esEs3(xv311, xv4011, bba)
new_esEs0(Right(xv310), Right(xv4010), gc, app(app(ty_Either, gg), gh)) → new_esEs0(xv310, xv4010, gg, gh)
new_esEs0(Left(xv310), Left(xv4010), app(ty_Maybe, ga), fc) → new_esEs2(xv310, xv4010, ga)
new_esEs1(@2(xv30, :(xv310, xv311)), @2(xv400, :(xv4010, xv4011)), he, app(ty_[], app(ty_[], bcb))) → new_esEs3(xv310, xv4010, bcb)
new_esEs1(@2(xv30, @3(xv310, xv311, xv312)), @2(xv400, @3(xv4010, xv4011, xv4012)), he, app(app(app(ty_@3, ba), app(ty_Maybe, de)), cg)) → new_esEs2(xv311, xv4011, de)
new_esEs1(@2(xv30, @3(xv310, xv311, xv312)), @2(xv400, @3(xv4010, xv4011, xv4012)), he, app(app(app(ty_@3, ba), app(app(ty_@2, dc), dd)), cg)) → new_esEs1(xv311, xv4011, dc, dd)
new_esEs1(@2(xv30, xv31), @2(xv400, xv401), he, app(app(ty_@2, hf), hg)) → new_esEs1(xv31, xv401, hf, hg)
new_esEs1(@2(xv30, Just(xv310)), @2(xv400, Just(xv4010)), he, app(ty_Maybe, app(app(app(ty_@3, hh), baa), bab))) → new_esEs(xv310, xv4010, hh, baa, bab)
new_esEs1(@2(xv30, Left(xv310)), @2(xv400, Left(xv4010)), he, app(app(ty_Either, app(ty_Maybe, ga)), fc)) → new_esEs2(xv310, xv4010, ga)
new_esEs0(Left(xv310), Left(xv4010), app(ty_[], gb), fc) → new_esEs3(xv310, xv4010, gb)
new_esEs1(@2(xv30, Left(xv310)), @2(xv400, Left(xv4010)), he, app(app(ty_Either, app(app(ty_Either, fd), ff)), fc)) → new_esEs0(xv310, xv4010, fd, ff)
new_esEs(@3(xv310, xv311, xv312), @3(xv4010, xv4011, xv4012), ba, bb, app(ty_[], cc)) → new_esEs3(xv312, xv4012, cc)
new_esEs1(@2(xv30, @3(xv310, xv311, xv312)), @2(xv400, @3(xv4010, xv4011, xv4012)), he, app(app(app(ty_@3, ba), bb), app(app(ty_Either, bf), bg))) → new_esEs0(xv312, xv4012, bf, bg)
new_esEs1(@2(xv30, Left(xv310)), @2(xv400, Left(xv4010)), he, app(app(ty_Either, app(app(app(ty_@3, eh), fa), fb)), fc)) → new_esEs(xv310, xv4010, eh, fa, fb)
new_esEs2(Just(xv310), Just(xv4010), app(app(ty_Either, bac), bad)) → new_esEs0(xv310, xv4010, bac, bad)
new_esEs0(Left(xv310), Left(xv4010), app(app(app(ty_@3, eh), fa), fb), fc) → new_esEs(xv310, xv4010, eh, fa, fb)
new_esEs(@3(xv310, xv311, xv312), @3(xv4010, xv4011, xv4012), app(app(ty_@2, ed), ee), bb, cg) → new_esEs1(xv310, xv4010, ed, ee)
new_esEs3(:(xv310, xv311), :(xv4010, xv4011), app(app(ty_Either, bbe), bbf)) → new_esEs0(xv310, xv4010, bbe, bbf)
new_esEs1(@2(xv30, Right(xv310)), @2(xv400, Right(xv4010)), he, app(app(ty_Either, gc), app(app(ty_Either, gg), gh))) → new_esEs0(xv310, xv4010, gg, gh)
new_esEs2(Just(xv310), Just(xv4010), app(ty_[], bah)) → new_esEs3(xv310, xv4010, bah)
new_esEs0(Left(xv310), Left(xv4010), app(app(ty_@2, fg), fh), fc) → new_esEs1(xv310, xv4010, fg, fh)
new_esEs(@3(xv310, xv311, xv312), @3(xv4010, xv4011, xv4012), app(ty_[], eg), bb, cg) → new_esEs3(xv310, xv4010, eg)
new_esEs(@3(xv310, xv311, xv312), @3(xv4010, xv4011, xv4012), app(app(ty_Either, eb), ec), bb, cg) → new_esEs0(xv310, xv4010, eb, ec)
new_esEs(@3(xv310, xv311, xv312), @3(xv4010, xv4011, xv4012), ba, app(app(ty_@2, dc), dd), cg) → new_esEs1(xv311, xv4011, dc, dd)
new_esEs1(@2(xv30, @3(xv310, xv311, xv312)), @2(xv400, @3(xv4010, xv4011, xv4012)), he, app(app(app(ty_@3, ba), bb), app(ty_[], cc))) → new_esEs3(xv312, xv4012, cc)
new_esEs1(@2(xv30, @3(xv310, xv311, xv312)), @2(xv400, @3(xv4010, xv4011, xv4012)), he, app(app(app(ty_@3, ba), app(app(ty_Either, da), db)), cg)) → new_esEs0(xv311, xv4011, da, db)
new_esEs1(@2(xv30, :(xv310, xv311)), @2(xv400, :(xv4010, xv4011)), he, app(ty_[], app(app(ty_@2, bbg), bbh))) → new_esEs1(xv310, xv4010, bbg, bbh)
new_esEs(@3(xv310, xv311, xv312), @3(xv4010, xv4011, xv4012), app(ty_Maybe, ef), bb, cg) → new_esEs2(xv310, xv4010, ef)
new_esEs0(Right(xv310), Right(xv4010), gc, app(app(app(ty_@3, gd), ge), gf)) → new_esEs(xv310, xv4010, gd, ge, gf)
new_esEs(@3(xv310, xv311, xv312), @3(xv4010, xv4011, xv4012), ba, bb, app(ty_Maybe, cb)) → new_esEs2(xv312, xv4012, cb)
new_esEs1(@2(xv30, @3(xv310, xv311, xv312)), @2(xv400, @3(xv4010, xv4011, xv4012)), he, app(app(app(ty_@3, app(ty_[], eg)), bb), cg)) → new_esEs3(xv310, xv4010, eg)
new_esEs1(@2(xv30, :(xv310, xv311)), @2(xv400, :(xv4010, xv4011)), he, app(ty_[], bba)) → new_esEs3(xv311, xv4011, bba)
new_esEs(@3(xv310, xv311, xv312), @3(xv4010, xv4011, xv4012), app(app(app(ty_@3, dg), dh), ea), bb, cg) → new_esEs(xv310, xv4010, dg, dh, ea)
new_esEs0(Left(xv310), Left(xv4010), app(app(ty_Either, fd), ff), fc) → new_esEs0(xv310, xv4010, fd, ff)
new_esEs(@3(xv310, xv311, xv312), @3(xv4010, xv4011, xv4012), ba, bb, app(app(ty_@2, bh), ca)) → new_esEs1(xv312, xv4012, bh, ca)
new_esEs2(Just(xv310), Just(xv4010), app(app(ty_@2, bae), baf)) → new_esEs1(xv310, xv4010, bae, baf)
new_esEs1(@2(xv30, @3(xv310, xv311, xv312)), @2(xv400, @3(xv4010, xv4011, xv4012)), he, app(app(app(ty_@3, app(app(app(ty_@3, dg), dh), ea)), bb), cg)) → new_esEs(xv310, xv4010, dg, dh, ea)
new_esEs1(@2(xv30, Right(xv310)), @2(xv400, Right(xv4010)), he, app(app(ty_Either, gc), app(app(ty_@2, ha), hb))) → new_esEs1(xv310, xv4010, ha, hb)
new_esEs1(@2(xv30, @3(xv310, xv311, xv312)), @2(xv400, @3(xv4010, xv4011, xv4012)), he, app(app(app(ty_@3, ba), bb), app(ty_Maybe, cb))) → new_esEs2(xv312, xv4012, cb)
new_esEs0(Right(xv310), Right(xv4010), gc, app(ty_Maybe, hc)) → new_esEs2(xv310, xv4010, hc)
new_esEs(@3(xv310, xv311, xv312), @3(xv4010, xv4011, xv4012), ba, app(app(ty_Either, da), db), cg) → new_esEs0(xv311, xv4011, da, db)
new_esEs3(:(xv310, xv311), :(xv4010, xv4011), app(app(ty_@2, bbg), bbh)) → new_esEs1(xv310, xv4010, bbg, bbh)
new_esEs1(@2(xv30, Just(xv310)), @2(xv400, Just(xv4010)), he, app(ty_Maybe, app(app(ty_@2, bae), baf))) → new_esEs1(xv310, xv4010, bae, baf)
new_esEs1(@2(xv30, Left(xv310)), @2(xv400, Left(xv4010)), he, app(app(ty_Either, app(ty_[], gb)), fc)) → new_esEs3(xv310, xv4010, gb)
new_esEs(@3(xv310, xv311, xv312), @3(xv4010, xv4011, xv4012), ba, app(app(app(ty_@3, cd), ce), cf), cg) → new_esEs(xv311, xv4011, cd, ce, cf)
new_esEs1(@2(xv30, @3(xv310, xv311, xv312)), @2(xv400, @3(xv4010, xv4011, xv4012)), he, app(app(app(ty_@3, ba), bb), app(app(app(ty_@3, bc), bd), be))) → new_esEs(xv312, xv4012, bc, bd, be)
new_esEs1(@2(xv30, Right(xv310)), @2(xv400, Right(xv4010)), he, app(app(ty_Either, gc), app(ty_[], hd))) → new_esEs3(xv310, xv4010, hd)
new_esEs1(@2(xv30, @3(xv310, xv311, xv312)), @2(xv400, @3(xv4010, xv4011, xv4012)), he, app(app(app(ty_@3, app(app(ty_@2, ed), ee)), bb), cg)) → new_esEs1(xv310, xv4010, ed, ee)
new_esEs1(@2(xv30, xv31), @2(xv400, xv401), app(app(ty_@2, bda), bdb), bcf) → new_esEs1(xv30, xv400, bda, bdb)
new_esEs1(@2(xv30, Right(xv310)), @2(xv400, Right(xv4010)), he, app(app(ty_Either, gc), app(ty_Maybe, hc))) → new_esEs2(xv310, xv4010, hc)
new_esEs1(@2(xv30, Left(xv310)), @2(xv400, Left(xv4010)), he, app(app(ty_Either, app(app(ty_@2, fg), fh)), fc)) → new_esEs1(xv310, xv4010, fg, fh)
new_esEs1(@2(xv30, :(xv310, xv311)), @2(xv400, :(xv4010, xv4011)), he, app(ty_[], app(app(app(ty_@3, bbb), bbc), bbd))) → new_esEs(xv310, xv4010, bbb, bbc, bbd)
new_esEs1(@2(xv30, :(xv310, xv311)), @2(xv400, :(xv4010, xv4011)), he, app(ty_[], app(ty_Maybe, bca))) → new_esEs2(xv310, xv4010, bca)
new_esEs1(@2(xv30, @3(xv310, xv311, xv312)), @2(xv400, @3(xv4010, xv4011, xv4012)), he, app(app(app(ty_@3, app(ty_Maybe, ef)), bb), cg)) → new_esEs2(xv310, xv4010, ef)
new_esEs(@3(xv310, xv311, xv312), @3(xv4010, xv4011, xv4012), ba, app(ty_[], df), cg) → new_esEs3(xv311, xv4011, df)
new_esEs1(@2(xv30, Just(xv310)), @2(xv400, Just(xv4010)), he, app(ty_Maybe, app(ty_[], bah))) → new_esEs3(xv310, xv4010, bah)
new_esEs1(@2(xv30, @3(xv310, xv311, xv312)), @2(xv400, @3(xv4010, xv4011, xv4012)), he, app(app(app(ty_@3, ba), bb), app(app(ty_@2, bh), ca))) → new_esEs1(xv312, xv4012, bh, ca)
new_esEs3(:(xv310, xv311), :(xv4010, xv4011), app(ty_Maybe, bca)) → new_esEs2(xv310, xv4010, bca)
new_esEs1(@2(xv30, Right(xv310)), @2(xv400, Right(xv4010)), he, app(app(ty_Either, gc), app(app(app(ty_@3, gd), ge), gf))) → new_esEs(xv310, xv4010, gd, ge, gf)
new_esEs1(@2(xv30, xv31), @2(xv400, xv401), app(app(app(ty_@3, bcc), bcd), bce), bcf) → new_esEs(xv30, xv400, bcc, bcd, bce)
new_esEs0(Right(xv310), Right(xv4010), gc, app(ty_[], hd)) → new_esEs3(xv310, xv4010, hd)
new_esEs(@3(xv310, xv311, xv312), @3(xv4010, xv4011, xv4012), ba, bb, app(app(app(ty_@3, bc), bd), be)) → new_esEs(xv312, xv4012, bc, bd, be)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ Narrow
            ↳ AND
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP
QDP
                ↳ QDPSizeChangeProof

Q DP problem:
The TRS P consists of the following rules:

new_foldr(xv3, :(xv40, xv41), ba, bb) → new_foldr(xv3, xv41, ba, bb)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: